eq(0, 0) → true
eq(0, s(X)) → false
eq(s(X), 0) → false
eq(s(X), s(Y)) → eq(X, Y)
rm(N, nil) → nil
rm(N, add(M, X)) → ifrm(eq(N, M), N, add(M, X))
ifrm(true, N, add(M, X)) → rm(N, X)
ifrm(false, N, add(M, X)) → add(M, rm(N, X))
purge(nil) → nil
purge(add(N, X)) → add(N, purge(rm(N, X)))
↳ QTRS
↳ DependencyPairsProof
eq(0, 0) → true
eq(0, s(X)) → false
eq(s(X), 0) → false
eq(s(X), s(Y)) → eq(X, Y)
rm(N, nil) → nil
rm(N, add(M, X)) → ifrm(eq(N, M), N, add(M, X))
ifrm(true, N, add(M, X)) → rm(N, X)
ifrm(false, N, add(M, X)) → add(M, rm(N, X))
purge(nil) → nil
purge(add(N, X)) → add(N, purge(rm(N, X)))
IFRM(false, N, add(M, X)) → RM(N, X)
PURGE(add(N, X)) → PURGE(rm(N, X))
EQ(s(X), s(Y)) → EQ(X, Y)
RM(N, add(M, X)) → EQ(N, M)
RM(N, add(M, X)) → IFRM(eq(N, M), N, add(M, X))
PURGE(add(N, X)) → RM(N, X)
IFRM(true, N, add(M, X)) → RM(N, X)
eq(0, 0) → true
eq(0, s(X)) → false
eq(s(X), 0) → false
eq(s(X), s(Y)) → eq(X, Y)
rm(N, nil) → nil
rm(N, add(M, X)) → ifrm(eq(N, M), N, add(M, X))
ifrm(true, N, add(M, X)) → rm(N, X)
ifrm(false, N, add(M, X)) → add(M, rm(N, X))
purge(nil) → nil
purge(add(N, X)) → add(N, purge(rm(N, X)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
IFRM(false, N, add(M, X)) → RM(N, X)
PURGE(add(N, X)) → PURGE(rm(N, X))
EQ(s(X), s(Y)) → EQ(X, Y)
RM(N, add(M, X)) → EQ(N, M)
RM(N, add(M, X)) → IFRM(eq(N, M), N, add(M, X))
PURGE(add(N, X)) → RM(N, X)
IFRM(true, N, add(M, X)) → RM(N, X)
eq(0, 0) → true
eq(0, s(X)) → false
eq(s(X), 0) → false
eq(s(X), s(Y)) → eq(X, Y)
rm(N, nil) → nil
rm(N, add(M, X)) → ifrm(eq(N, M), N, add(M, X))
ifrm(true, N, add(M, X)) → rm(N, X)
ifrm(false, N, add(M, X)) → add(M, rm(N, X))
purge(nil) → nil
purge(add(N, X)) → add(N, purge(rm(N, X)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
EQ(s(X), s(Y)) → EQ(X, Y)
eq(0, 0) → true
eq(0, s(X)) → false
eq(s(X), 0) → false
eq(s(X), s(Y)) → eq(X, Y)
rm(N, nil) → nil
rm(N, add(M, X)) → ifrm(eq(N, M), N, add(M, X))
ifrm(true, N, add(M, X)) → rm(N, X)
ifrm(false, N, add(M, X)) → add(M, rm(N, X))
purge(nil) → nil
purge(add(N, X)) → add(N, purge(rm(N, X)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
EQ(s(X), s(Y)) → EQ(X, Y)
The value of delta used in the strict ordering is 1/4.
POL(EQ(x1, x2)) = (1/2)x_1
POL(s(x1)) = 1/2 + (4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
eq(0, 0) → true
eq(0, s(X)) → false
eq(s(X), 0) → false
eq(s(X), s(Y)) → eq(X, Y)
rm(N, nil) → nil
rm(N, add(M, X)) → ifrm(eq(N, M), N, add(M, X))
ifrm(true, N, add(M, X)) → rm(N, X)
ifrm(false, N, add(M, X)) → add(M, rm(N, X))
purge(nil) → nil
purge(add(N, X)) → add(N, purge(rm(N, X)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
IFRM(false, N, add(M, X)) → RM(N, X)
RM(N, add(M, X)) → IFRM(eq(N, M), N, add(M, X))
IFRM(true, N, add(M, X)) → RM(N, X)
eq(0, 0) → true
eq(0, s(X)) → false
eq(s(X), 0) → false
eq(s(X), s(Y)) → eq(X, Y)
rm(N, nil) → nil
rm(N, add(M, X)) → ifrm(eq(N, M), N, add(M, X))
ifrm(true, N, add(M, X)) → rm(N, X)
ifrm(false, N, add(M, X)) → add(M, rm(N, X))
purge(nil) → nil
purge(add(N, X)) → add(N, purge(rm(N, X)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
IFRM(false, N, add(M, X)) → RM(N, X)
IFRM(true, N, add(M, X)) → RM(N, X)
Used ordering: Polynomial interpretation [25,35]:
RM(N, add(M, X)) → IFRM(eq(N, M), N, add(M, X))
The value of delta used in the strict ordering is 1/4.
POL(add(x1, x2)) = 1/4 + (4)x_2
POL(RM(x1, x2)) = x_2
POL(eq(x1, x2)) = (1/4)x_2
POL(true) = 0
POL(false) = 0
POL(s(x1)) = (2)x_1
POL(IFRM(x1, x2, x3)) = x_3
POL(0) = 1/4
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
RM(N, add(M, X)) → IFRM(eq(N, M), N, add(M, X))
eq(0, 0) → true
eq(0, s(X)) → false
eq(s(X), 0) → false
eq(s(X), s(Y)) → eq(X, Y)
rm(N, nil) → nil
rm(N, add(M, X)) → ifrm(eq(N, M), N, add(M, X))
ifrm(true, N, add(M, X)) → rm(N, X)
ifrm(false, N, add(M, X)) → add(M, rm(N, X))
purge(nil) → nil
purge(add(N, X)) → add(N, purge(rm(N, X)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
PURGE(add(N, X)) → PURGE(rm(N, X))
eq(0, 0) → true
eq(0, s(X)) → false
eq(s(X), 0) → false
eq(s(X), s(Y)) → eq(X, Y)
rm(N, nil) → nil
rm(N, add(M, X)) → ifrm(eq(N, M), N, add(M, X))
ifrm(true, N, add(M, X)) → rm(N, X)
ifrm(false, N, add(M, X)) → add(M, rm(N, X))
purge(nil) → nil
purge(add(N, X)) → add(N, purge(rm(N, X)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
PURGE(add(N, X)) → PURGE(rm(N, X))
The value of delta used in the strict ordering is 1/16.
POL(add(x1, x2)) = 1/4 + (4)x_2
POL(eq(x1, x2)) = 0
POL(true) = 0
POL(rm(x1, x2)) = x_2
POL(false) = 0
POL(s(x1)) = 0
POL(ifrm(x1, x2, x3)) = x_3
POL(0) = 0
POL(nil) = 1/2
POL(PURGE(x1)) = (1/4)x_1
rm(N, nil) → nil
ifrm(true, N, add(M, X)) → rm(N, X)
rm(N, add(M, X)) → ifrm(eq(N, M), N, add(M, X))
ifrm(false, N, add(M, X)) → add(M, rm(N, X))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
eq(0, 0) → true
eq(0, s(X)) → false
eq(s(X), 0) → false
eq(s(X), s(Y)) → eq(X, Y)
rm(N, nil) → nil
rm(N, add(M, X)) → ifrm(eq(N, M), N, add(M, X))
ifrm(true, N, add(M, X)) → rm(N, X)
ifrm(false, N, add(M, X)) → add(M, rm(N, X))
purge(nil) → nil
purge(add(N, X)) → add(N, purge(rm(N, X)))